\begin{tabbing}
once{-}p(${\it es}$;$i$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=existse{-}at(${\it es}$; $i$; $e$.(es{-}kind(${\it es}$; $e$) $=$ locl($a$) $\in$ Knd))\+
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.alle{-}at(${\it es}$;$i$;${\it e'}$.\=es{-}kind(${\it es}$; $e$) $=$ locl($a$) $\in$ Knd\+
\\[0ex]$\Rightarrow$ es{-}kind(${\it es}$; ${\it e'}$) $=$ locl($a$) $\in$ Knd
\\[0ex]$\Rightarrow$ $e$ $=$ ${\it e'}$ $\in$ es{-}E(${\it es}$)))
\-\-
\end{tabbing}